/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import java.io.BufferedWriter;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.HashMap;
import java.util.Map;

import alloy.util.Dbg;

/**
 * Visitor used by {@link BooleanFormula#writeBLIF} to write a BLIF for an array
 * of Boolean formulas.  This visitor is invoked to write the circuit nodes for
 * one Boolean formula.  The same visitor is run on all Boolean formulas in the array,
 * so that for shared subformulas only one circuit node is created.
 * <p>
 * The BooleanFormula must consist exclusively of AND/OR/NOT/LIT nodes.
 */
class WriteBLIF_V extends GBF_V {
    /**
     * BLIF file which we're writing
     */
    private PrintWriter _w;
    
    /**
     * Map from BooleanFormula node to gate name.
     */
    Map /* BooleanFormula->String */ _bfnode2gateName = new HashMap();

    /** Next node id to assign */
    int nextNodeId = 1;

    /////////////
    // Methods //
    /////////////

    WriteBLIF_V(String fname_, int nvars_, BooleanFormula[] outputs_) {
	try {
	    _w = new PrintWriter(new BufferedWriter(new FileWriter(fname_)));
	} catch (IOException ioe_) {
	    throw new Error("could not open blif file for writing");
	}
	_w.println(".model mymodel");
	_w.print(".inputs");
	for (int i=1; i<=nvars_; i++) {
	    String inpName = "i" + i; 
	    _w.print(" " + inpName);
	    _setGateName(BooleanFormula.makeLit(i), inpName);
	}
	_w.println();
	_w.print(".outputs ");
	for (int i = 1; i<=outputs_.length; i++) {
	    String outName = "o" + i;
	    _w.print(" " + outName);
	    _setGateName(outputs_[i-1], outName);
	}
	_w.println();
    }

    void close() { _w.println(".end"); _w.close(); _w = null; } 

    private void _setGateName(BooleanFormula bf_, String gateName_) {
	Dbg.chk(_getGateName(bf_) == null);
	_bfnode2gateName.put(bf_, gateName_);
    }

    private String _getGateName(BooleanFormula bf_) {
	return (String)_bfnode2gateName.get(bf_);
    }

    private boolean _isOutput(BooleanFormula bf_) {
	return _getGateName(bf_) != null &&
	    _getGateName(bf_).startsWith("o");
    }

    private boolean _checkSeen(BooleanFormula bf_) {
	if (_getGateName(bf_) != null)
	    return true;
	else {
	    if (_getGateName(bf_) == null) {
		String gateName = "g" + (nextNodeId++);
		_setGateName(bf_, gateName);
	    }
	    return false;
	}
    }

    Object forLit(GBF_Lit lit_) {
	if (_getGateName(lit_) == null) {
	    Dbg.chk(lit_.getLit() < 0);
	    _checkSeen(lit_); // generate a gate name
	    _w.println(".table " + _getGateName(lit_.opposite()) + " -> " +
		       _getGateName(lit_));
	    _w.println("0 1"); 
	    _w.println("1 0"); 
	}
	return null;
    }
    Object forNot(GBF_Not not_) {
	if (_isOutput(not_) || !_checkSeen(not_)) {
	    not_.getExpr().acceptVisitor(this);
	    _w.println(".table " + _getGateName(not_.getExpr()) +
		       " -> " + _getGateName(not_));
	    _w.println("0 1");
	    _w.println("1 0");
	}
	return null;
    }

    private Object _forAndOr(GBF_AndOrBase andor_, boolean isAnd_) {
	if (_isOutput(andor_) || !_checkSeen(andor_)) {
	    BooleanFormula[] subs = andor_.subexprs;
	    for (int i=0; i<subs.length; i++)
		subs[i].acceptVisitor(this);
	    _w.print(".table");
	    for (int i=0; i<subs.length; i++)
		_w.print(" " + _getGateName(subs[i]));
	    _w.println(" -> " + _getGateName(andor_));
	    _w.println(".default 0");
	    if (isAnd_) {
		for (int i=0; i<subs.length; i++)
		    _w.print("1 ");
		_w.println(" 1");
	    } else {
		for (int i=0; i<subs.length; i++) {
		    for (int j=0; j<subs.length; j++) {
			_w.print(j==i ? '1' : '-');
			_w.print(" ");
		    }
		    _w.println(" 1");
		}
	    }
	}
	return null;
    }

    Object forAnd(GBF_And and_) { return _forAndOr(and_, true); }
    Object forOr(GBF_Or or_) { return _forAndOr(or_, false); }
    Object forConst(GBF_Const const_) {
	if (!_checkSeen(const_)) {
	    _w.println(".table " + _getGateName(const_));
	    if (const_ == BooleanFormula.TRUE())
		_w.println(".default 1");
	    else
		_w.println(".default 0");
	}
	return null;
    }

    Object forVarConst(VarConst varConst_) {
	throw new Error("bad node");
    }
    
    Object forSetVarExpr(SetVarExpr setVarExpr_) {
	throw new Error("bad node");
    }

    Object forCNFFunc(CNFFunc cnfFunc_) { throw new Error("bad node"); }
}
